Nuprl Definition : combine-ecl-tuples
0,22
postcript
pdf
combine-ecl-tuples(
A
;
B
;
f
;
g
)
== let
Ta
,
ksa
,
ia
,
ga
,
ha
,
aa
,
ae
=
A
in
==
let
Tb
,
ksb
,
ib
,
gb
,
hb
,
ab
,
be
=
B
in
==
<(
Ta
Tb
)
==
,(
ksa
@
ksb
)
==
,<
ia
,
ib
>
==
,(
k'
,
s
,
v
,
x
. <if deq-member(KindDeq;
k'
;
ksa
)
ga
(
k'
,
s
,
v
,1of(
x
)) else 1of(
x
) fi
== ,(
k'
,
s
,
v
,
x
.
,if deq-member(KindDeq;
k'
;
ksb
)
ha
(0,1of(
x
))
gb
(
k'
,
s
,
v
,2of(
x
)) else 2of(
x
) fi>)
==
,(
n
,
x
.
f
((
m
.
ha
(
m
,1of(
x
))),
m
.
hb
(
m
,2of(
x
)),
n
))
==
,(
n
,
k'
,
s
,
v
,
x
.
g
== ,(
n
,
k'
,
s
,
v
,
x
.
(if deq-member(KindDeq;
k'
;
ksa
)
aa
(
n
,
k'
,
s
,
v
,1of(
x
)) else false
fi
== ,(
n
,
k'
,
s
,
v
,
x
.
,if deq-member(KindDeq;
k'
;
ksb
)
ha
(0,1of(
x
))
ab
(
n
,
k'
,
s
,
v
,2of(
x
))
== ,(
n
,
k'
,
s
,
v
,
x
. ,
else false
fi))
==
,merge(
ae
;
be
)>
latex
Definitions
let
a
,
b
,
c
,
d
,
e
,
f
,
g
=
u
in
v
(
a
;
b
;
c
;
d
;
e
;
f
;
g
)
,
as
@
bs
,
if
b
t
else
f
fi
,
deq-member(
eq
;
x
;
L
)
,
KindDeq
,
p
q
,
1of(
t
)
,
2of(
t
)
,
false
,
merge(
as
;
bs
)
FDL editor aliases
combine-ecl-tuples
origin